(declare-fun i1 () Int)
(declare-fun str0 () String)
(declare-fun str3 () String)
(declare-fun str4 () String)
(declare-fun str5 () String)
(declare-fun str6 () String)
(declare-fun i6 () Int)
(push)
(assert (str.suffixof (str.from_int 831) (str.++ "" (str.from_int (- (- (str.len str5) 78) 831)) str5)))
(assert (str.prefixof str5 ""))
(assert (or (= i6 0) (or (< 0 (- 0 0 0 (div i1 (* 831 (str.len str6)))) 941 i6 0) (distinct str4 (str.++ "" (str.from_int (- (- (str.len str5) 78) 831)) str5) str3 "" str0))))
(check-sat)
